package explorer.driver;

import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Stack;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

import solver.SatProblem;
import solver.Util;
import explorer.backtracker.Backtracker;
import explorer.exception.InternalTimeoutException;
import explorer.exception.InvalidConfigurationException;
import explorer.exception.InvalidFeatureModelException;

public class Driver {

  public static boolean DEBUG = true;
  boolean fixedFeatures = false;
  public static long TOTAL_TIMER = 0;
  public static long CONST_SOLVER_TIMER = 0;

  public static boolean exceptionRaised = false;
  public static boolean createConfigurationsFile = false; //
  public static boolean callSystemCurrentTime = false;
  int cnfLength;
  public ArrayList<String> leafConfigurations;

  private long cs_time = 0;
  private long total_time = 0;

  Code code; // code for analysis
  SatProblem problem; // query
  int size; // number of variable in query
  public ISolver solver; // solver interface

  Backtracker bt = Backtracker.getSingleton();

  /**
   * symbolic state
   */
  int[] initSymState;
  int[] symState;
  ArrayList<int[]> validExecutions;
  ArrayList<int[]> invalidExecutions;
  ArrayList<int[]> validLeafExecutions;

  int numberValidExecutions = 0;
  int numberInvalidExecutions = 0;

  List<IConstr> observedConstraints = new ArrayList<IConstr>();

  public static int[] featuresToBeActivated = new int[]{10,
    11,
    12,
    13,
    14,
    20,
    19,
    18,
    17,
    15,
    36,
    35,
    34,
    32,
    31,
    30,
    29,
    26,
    25,
    22,
    55,
    54,
    53,
    52,
    50,
    49,
    48,
    47,
    45,
    43,
    42,
    41,
    40,
    38,
    37};
  
  public Driver(Code code, String strFM_File) throws IOException,
      ClassNotFoundException {
    this.code = code;
    validExecutions = new ArrayList<int[]>();
    invalidExecutions = new ArrayList<int[]>();
    validLeafExecutions = new ArrayList<int[]>();
    // initializing and creating the sat4j solver
    problem = SatProblem.load(strFM_File);
    size = problem.featureVariables.size() + 1;
    if (DEBUG) {
      System.out.println("---------------");
      System.out.println(problem.toString());
      System.out.println("---------------");
    }
    initSymState = new int[size];
    symState = new int[size];
    Arrays.fill(initSymState, -1);
//    LOGGING_FINER = 3;
//    LOGGING_CONFIG = 4;
//    LOGGING_SEVERE = 5;
    int[] fixedFeatures = util.util.fixedFeatures;
    if(this.fixedFeatures) {
      for(int i = 0; i < fixedFeatures.length; i++) {
        initSymState[fixedFeatures[i]] = 1;
      }
    }
    
//    initSymState[10] = 1;
//    initSymState[11] = 1;
//    initSymState[12] = 1;
//    initSymState[13] = 1;
//    initSymState[14] = 1;
//    initSymState[20] = 1;
//    initSymState[19] = 1;
//    initSymState[18] = 1;
//    initSymState[17] = 1;
//    initSymState[15] = 1;
//    initSymState[36] = 1;
//    initSymState[35] = 1;
//    initSymState[34] = 1;
//    initSymState[32] = 1;
//    initSymState[25] = 1;
//    initSymState[22] = 1;
//    initSymState[55] = 1;
//    initSymState[54] = 1;
//    initSymState[53] = 1;
//    initSymState[52] = 1;
//    initSymState[50] = 1;
//    initSymState[49] = 1;
//    initSymState[48] = 1;
//    initSymState[47] = 1;
//    initSymState[45] = 1;
//    initSymState[43] = 1;
//    initSymState[42] = 1;
//    initSymState[41] = 1;
//    initSymState[40] = 1;
//    initSymState[38] = 1;
//    initSymState[37] = 1;
  }

  /**
   * this is part of the infrastructure; the driver that will explore the
   * distinct paths with re-execution.
   **/

  // boolean withinFinally;
  // public void setIsWithinFinally(boolean val) {
  // withinFinally = val;
  // }

  Stack<Boolean> finallies = new Stack<Boolean>();

  private boolean isInFinally() {
    return !finallies.isEmpty();
  }

  public void pushFinally() {
    finallies.push(true);
  }

  public void popFinally() {
    finallies.pop();
  }

  int id1_Old;
  boolean raisedException = false;

  // part of infra-structure: decision on feature selection
  public synchronized boolean choose(int featureIndex) {
    // DEFENSIVE PROGRAMMING
    if (raisedException && id1_Old == configurationId) {
      /**
       * we get to this point if application raised one of our exceptions but
       * that was captured (either through catch or finally)
       */
      if (isInFinally()) {
        /**
         * in case it came from finally just continue with any value. the
         * exception has been re-raised already (see block below)
         */
        return true /* don't care */;
      } else {
        /**
         * this block of defensive code enforces us to re-raise an exception of
         * our kind in case that was captured by the application code.
         */
        System.out.println(Arrays.toString(symState));
        System.err
            .println("Your application code is capturing our exception.  Please, adjust that!");
        (new RuntimeException()).printStackTrace(); // does not leave this stmt
        System.exit(-1);
      }
    }
    id1_Old = configurationId;
    raisedException = true;
    // =========CONSTRAINT SOLVER==========
    if (callSystemCurrentTime)
      cs_time = System.currentTimeMillis();
    boolean result;
    int enabled = symState[featureIndex];
    if (enabled == -1 /* UNKNOWN */) {
      result = bt.choose();
      int val = (result ? 1 : 0);
      symState[featureIndex] = val;
      // query sat solver
      int constraint = result ? featureIndex : -featureIndex;
      try {
        IConstr iconstr = solver
            .addClause(new VecInt(new int[] { constraint }));
        if (iconstr != null) {
          observedConstraints.add(iconstr);
        }
        try {
          if (!solver.isSatisfiable()) {
            throw new InvalidConfigurationException();
          }
        } catch (TimeoutException e) {
          throw new InternalTimeoutException();
        }
      } catch (ContradictionException e) {
        throw new InvalidConfigurationException();
      } finally {
        if (callSystemCurrentTime) {
          CONST_SOLVER_TIMER += System.currentTimeMillis() - cs_time;
        }
      }
    } else {
      result = (enabled == 1);
    }
    raisedException = false;
    return result;
    // ====================================
  }

  /**
   * Creating and initializing the sat4j solver
   * 
   * @param famaModel
   *          TODO
   * @throws ClassNotFoundException
   * @throws IOException
   */

  public ISolver createSolver(int numVars) {
    ISolver result;
    result = solver = SolverFactory.newDefault();
    // prepare the solver to accept MAXVAR variables . MANDATORY
    solver.newVar(numVars);
    return result;
  }

  /**
   * part of infra-structure: decision on feature selection
   * 
   * this is app-specific
   * 
   * @throws TimeoutException
   **/
  public void checkModelValidity(SatProblem problem) throws TimeoutException {
    boolean result;
    result = solver.isSatisfiable();
    if (!result) {
      throw new InvalidFeatureModelException();
    }
    if (DEBUG) {
      System.out.println(result ? "Model is Valid"
          : "Model may not be Valid (due to timeout)");
      System.out.println("------------------------------------");
    }
  }

  private void loadModel(SatProblem problem) {
    List<String> clauses = problem.clauses;
    // convert problem.clauses (list of string) into various arrays of ints.
    // one array for each clause
    Iterator<String> it = clauses.iterator();
    while (it.hasNext()) {
      int[] array = Util.dimacsClauseToIntArray(it.next());
      try {
        solver.addClause(new VecInt(array));
      } catch (ContradictionException e) {
        // Got a contradiction but should continue with the execution
        e.printStackTrace();
      }
    }
  }

  static class MyThread extends Thread {
    Code code;
    Throwable throwable;

    MyThread(Code code) {
      this.code = code;
    }

    public void run() {
      try {
        code.run();
      } catch (Throwable _) {
        throwable = _;
      }
    }
  }

  int configurationId = 0;

  public void analyze(ArrayList<int[]> configurations) throws IOException,
      ClassNotFoundException {
    long timeOut = 60000;
    
    total_time = System.currentTimeMillis();
    leafConfigurations = new ArrayList<String>();
    CONST_SOLVER_TIMER = 0;
    solver = createSolver(size);
    boolean firstTime = true;

    do {
//      if(System.currentTimeMillis() - total_time > timeOut) {
//        break;
//      }
      
      boolean isValidConfiguration = true;
      boolean isNormalExecution = true;

      System.out.println(configurationId + 1);
      try {

        // RESTORE STATE STARTS
        /****** OPTION 0: recreate solver state (potentially expensive) *******/

        // =========CONSTRAINT SOLVER==========
        if (callSystemCurrentTime) {
          cs_time = System.currentTimeMillis();
        }
        solver.reset();

        if (firstTime) {
          loadModel(problem);
          checkModelValidity(problem);
          firstTime = false;
        }
        if (callSystemCurrentTime) {
          CONST_SOLVER_TIMER += System.currentTimeMillis() - cs_time;
        }
        // ====================================

        /****** OPTION 1: a bit more efficient *******/
         for (IConstr constr : observedConstraints) {
         solver.removeConstr(constr);
         }
         observedConstraints.clear();

        // symbolic state is restored on entry
        if (configurations == null) {
          System.arraycopy(initSymState, 0, symState, 0, size);
        }
        // RESTORE STATE ENDS

        exceptionRaised = false;

        // Setting configuration in case it exist
        if (configurations != null) {
          if (configurationId == configurations.size()) {
            break;
          }
          System.arraycopy(configurations.get(configurationId), 0, symState, 0,
              size);
        }
        configurationId++;
        
        // Adding clauses in case feature were setted: RQ4
//        if(featuresToBeActivated != null) {
//          for(int i = 0; i < featuresToBeActivated.length; i++) {
//            choose(featuresToBeActivated[i]);
//          }
//        }
        for(int i = 0; i < symState.length; i++) {
          if(symState[i] != -1) {
            int constraint = (symState[i] == 1) ? i : -i;
            IConstr iconstr = solver
                .addClause(new VecInt(new int[] { constraint }));
            if (iconstr != null) {
              observedConstraints.add(iconstr);
            }
            try {
              if (!solver.isSatisfiable()) {
                throw new InvalidConfigurationException();
              }
            } catch (TimeoutException e) {
              throw new InternalTimeoutException();
            }
          }
        }
        // =========EXECUTION==========

        // code.run();
        /**
         * THREAD CODE, to use with BERKLEYDB
         */
//        while (Thread.currentThread().activeCount() > 1) {
//          System.out
//              .println("One or more threads other than the main Thread is/are open: "
//                  + Thread.currentThread().activeCount());
//          Thread.sleep(10);
//        }

        MyThread mt = new MyThread(code);
        mt.start();
        mt.join(150000000);
        if (mt.throwable != null) {
          throw mt.throwable;
        }
      } catch (InvalidConfigurationException _) {
        // launched whenever a trivial contradiction is found (e.g. null
        // clause).
        // System.err.println("Contradiction Exception ");
        isValidConfiguration = false;
        raisedException = false;
      } catch (InternalTimeoutException _) {
        System.err.println("INTERNAL TIMEOUT");
        isValidConfiguration = false;
        raisedException = false;
      } catch (TimeoutException _) {
        System.err.println("TIMEOUT");
        isValidConfiguration = false;

      } catch (InvalidFeatureModelException _) {
        System.err.println("INVALID FEATURE MODEL");
        isValidConfiguration = false;

      } catch (Throwable _) {
        try {
          if (!solver.isSatisfiable()) {
            isValidConfiguration = false;
          }
        } catch (TimeoutException e) {
          System.err.println("TIMEOUT");
          isValidConfiguration = false;
        }
        isNormalExecution = false;

      } finally {

        int[] solution = null;

        if (isValidConfiguration && !exceptionRaised) {
          try {
            long cs_time = 0;
            if (callSystemCurrentTime) {
              cs_time = System.currentTimeMillis();
            }
            solution = solver.findModel();
            if (solution == null) {
              System.err.println("FATAL ERROR!");

              if (!solver.isSatisfiable()) {
                System.out.println("NAO ENTENDO!");
              }

              System.exit(0);
            }
            if (callSystemCurrentTime) {
              CONST_SOLVER_TIMER += System.currentTimeMillis() - cs_time;
            }
          } catch (TimeoutException e) {
            System.err
                .println("UNEXPECTED -- failed to find a model at the end of a path");
          } finally {
            if (solution != null) {
              for (int i = 0; i < solution.length; i++) {
                if (solution[i] < 0) {
                  solution[i] = 0;
                } else {
                  solution[i] = 1;
                }
              }
              // Util operation may cost a lot.
              solution = Util.addingZeroElementArray(solution);
              for(int i = 0; i < solution.length; i++) {
                if(symState[i] != -1) {
                  solution[i] = symState[i];
                }
              }
              validExecutions.add(solution.clone());
              numberValidExecutions++;
            }
          }
        }

        if (solution == null) {
          numberInvalidExecutions++;
        }
        List<Integer> partialState = getPartialState();
        // if(solution != null) {
        // leafConfigurations.add(getLeafConfiguration(partialState));
        // }
        if (DEBUG) {
          // List<Integer> partialState = new ArrayList<Integer>();
          // for (int i = 0; i < symState.length; i++) {
          // if (symState[i] == 0) {
          // partialState.add(-i);
          // } else if (symState[i] == 1) {
          // partialState.add(i);
          // }
          // }

          if (solution != null) {
          }
          // System.out.printf("[%s,%s]:\n " + "symState var (dense): %s\n "
          // + "symState var (sparse): %s\n " + "SAT4J solution: %s\n",
          // isValidConfiguration ? "V" : "I", isNormalExecution ? "N" : "E",
          // Arrays.toString(symState), partialState,
          // (solution != null) ? Arrays.toString(solution) : "UNSAT");
        }
      }

      // find next configuration to explore
      cnfLength += solver.nConstraints();
      System.out.println(Arrays.toString(symState));
      bt.backtrack();
    } while (bt.hasMore()
        || (configurations != null && configurationId != configurations.size()));
    System.out
        .println("====================Measuring Time=======================");
    TOTAL_TIMER = System.currentTimeMillis() - total_time;
    System.out.println("\nTOTAL_TIME---> " + TOTAL_TIMER);
    System.out.println("TIME_CONST_SOLVER---> " + CONST_SOLVER_TIMER);

    System.out.println("===========================================");
    System.out.println("Number of VALID executions: " + numberValidExecutions);
    System.out.println("Number of INVALID executions: "
        + numberInvalidExecutions);
    System.out.println("Number of TOTAL executions: "
        + (numberInvalidExecutions + numberValidExecutions));
    System.out.println("All valid executions SET: ");
    if (configurations == null) {
      for (int[] validExecution : validExecutions) {
        System.out.println(Arrays.toString(validExecution));
      }
    }
    if(validExecutions.size() + invalidExecutions.size() == 0) {
      System.out.println("CNF LENGTH = 0");
    } else {
      System.out.println("CNF LENGTH = " + cnfLength/(validExecutions.size() + invalidExecutions.size()));
    }

    // In case you need to generate a file containing all valid configurations
    // Run the line below
    if (createConfigurationsFile)
      Util.createFeaturesFile(leafConfigurations, "sudoku.txt");

  }

  private String getLeafConfiguration(List<Integer> partialState) {
    StringBuffer leaf = new StringBuffer();
    // INVERT THE MAP from FEATURENAME:FEATUREINDEX to FEATUREINDEX:FEATURENAME
    Map<String, String> invertedMap = Util.invert(problem.featureVariables);
    for (int i : partialState) {
      if (i > 0) {
        leaf.append(invertedMap.get(String.valueOf(i)) + " ");
      }
    }
    return leaf.toString();
  }

  private List<Integer> getPartialState() {
    List<Integer> partialState = new ArrayList<Integer>();
    for (int i = 0; i < symState.length; i++) {
      if (symState[i] == 0) {
        partialState.add(-i);
      } else if (symState[i] == 1) {
        partialState.add(i);
      }
    }
    return partialState;
  }

  public ArrayList<int[]> getValidConfigurations() {
    return validExecutions;
  }

  public int getValidExecutionsNumber() {
    return numberValidExecutions;
  }

  public int getInvalidExecutionsNumber() {
    return numberInvalidExecutions;
  }
  
  public int getCNFLength() {
    return cnfLength;
  }

}
